(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const i8 Int)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert (or (<= 124 i6) v11 (xor (not (or v4 v4 v1)) (or v4 v4 v1) v5 (>= i0 102))))
(assert (or v6 (< (div i1 (div i3 27)) (mod i3 102)) v0))
(assert (or v3 (or v4 v4 v1) v9))
(assert (or (<= 124 i6) (>= i6 i7) (xor (not (or v4 v4 v1)) (or v4 v4 v1) v5 (>= i0 102))))
(assert (or v9 v11 v9))
(assert (or v11 (xor (not (or v4 v4 v1)) (or v4 v4 v1) v5 (>= i0 102)) v7))
(assert (or (= i1 (- i0)) (< (div i1 (div i3 27)) (mod i3 102)) v9))
(assert (or (= (* 172 (+ 102 i1 i4 i1) i3 i0 i0) (div i3 27)) (or v4 v4 v1) v11))
(assert (or v9 (< (div i1 (div i3 27)) (mod i3 102)) (>= i6 i7)))
(assert (or v3 v7 (= (* 172 (+ 102 i1 i4 i1) i3 i0 i0) (div i3 27))))
(assert (or v3 (= 102 (+ 102 i1 i4 i1)) (>= i6 i7)))
(assert (or v7 (<= 124 i6) (<= 124 i6)))
(assert (or (< (div i1 (div i3 27)) (mod i3 102)) (xor (not (or v4 v4 v1)) (or v4 v4 v1) v5 (>= i0 102)) (= (* 172 (+ 102 i1 i4 i1) i3 i0 i0) (div i3 27))))
(assert (or v3 (>= i6 i7) v11))
(assert (or (>= i6 i7) v6 (or v4 v4 v1)))
(assert (or (<= 124 i6) v6 (= 102 (+ 102 i1 i4 i1))))
(assert (or v7 v6 (>= i0 102)))
(assert (or v7 (= 102 (+ 102 i1 i4 i1)) (<= 124 i6)))
(assert (or (= i1 (- i0)) (or v4 v4 v1) v0))
(assert (or v3 v3 v9))
(assert (or (= 102 (+ 102 i1 i4 i1)) (= 102 (+ 102 i1 i4 i1)) (= i1 (- i0))))
(assert (or (>= i0 102) v3 (>= i6 i7)))
(assert (or v0 (<= 124 i6) (<= 124 i6)))
(assert (or (or v4 v4 v1) (= (* 172 (+ 102 i1 i4 i1) i3 i0 i0) (div i3 27)) (or v4 v4 v1)))
(assert (or (>= i0 102) (< (div i1 (div i3 27)) (mod i3 102)) (< (div i1 (div i3 27)) (mod i3 102))))
(assert (or (= 102 (+ 102 i1 i4 i1)) v0 v0))
(assert (or v9 v9 (>= i6 i7)))
(assert (or v9 (= i1 (- i0)) v0))
(assert (or v11 (or v4 v4 v1) v11))
(assert (or v0 v7 (= 102 (+ 102 i1 i4 i1))))
(assert (or (= i1 (- i0)) v7 v6))
(assert (or (>= i0 102) (>= i6 i7) (>= i0 102)))
(assert (or v7 (>= i6 i7) v3))
(assert (or (>= i6 i7) (>= i6 i7) v7))
(assert (or (or v4 v4 v1) (= i1 (- i0)) v9))
(assert (or (= (* 172 (+ 102 i1 i4 i1) i3 i0 i0) (div i3 27)) v3 (<= 124 i6)))
(assert (or v11 v3 v6))
(assert (or (or v4 v4 v1) v3 (xor (not (or v4 v4 v1)) (or v4 v4 v1) v5 (>= i0 102))))
(assert (or (>= i6 i7) v6 (>= i0 102)))
(assert (or (= 102 (+ 102 i1 i4 i1)) v7 (= 102 (+ 102 i1 i4 i1))))
(assert (or (< (div i1 (div i3 27)) (mod i3 102)) v0 (xor (not (or v4 v4 v1)) (or v4 v4 v1) v5 (>= i0 102))))
(assert (or (= i1 (- i0)) v3 v6))
(assert (or (>= i6 i7) (= i1 (- i0)) (= i1 (- i0))))
(check-sat)
